2021-04-11 03:39:33 (CEST) cTI start

% cTI_lt 0.25 using 23.619 MLIPS SICStus 3.8.5 (x86-linux-glibc2.1): Mon Oct 30 16:34:14 CET 2000.
% cTI: Rt=92ms, Wt=90ms. NTI: Rt=8ms, Wt=6ms at most 77 inferences for useful informations.
% NTI summary:  Complete result is optimal.
som3(A,B,C)terminates_if b(A);b(B);b(C).
    % optimal. loops found: [som3([A|_],[B|_],[A+B|_])]. NTI took    0ms,72i,72i
som4_1(A,B,C,D)terminates_if b(A),b(B);b(A),b(C);b(A),b(D);b(B),b(C);b(B),b(D).
    % optimal. loops found: [som4_1([],[A|_],[B|_],[A+B|_]),som4_1([C|_],[],[D|_],[C+D|_]),som4_1([_|_],[_|_],y,y)]. NTI took    0ms,77i,77i
som4_2(A,B,C,D)terminates_if b(A),b(C);b(B),b(C);b(D).
    % optimal. loops found: [som4_2([A|_],[B|_],[],[A+B|_]),som4_2(y,y,[C|_],[_+C|_])]. NTI took    4ms,76i,76i

% Comparison with termination analyzers
% A termination analyser of identical power would verify
% with the following 17 proofs the 3 inferred conditions:

som3(f, f, b).
    % ==> termination proof established
som3(f, b, f).
    % ==> termination proof established
som3(b, f, f).
    % ==> termination proof established
som3(f, f, f).
    % ==> no proof found
som4_1(f, b, f, b).
    % ==> termination proof established
som4_1(f, b, b, f).
    % ==> termination proof established
som4_1(b, f, f, b).
    % ==> termination proof established
som4_1(b, f, b, f).
    % ==> termination proof established
som4_1(b, b, f, f).
    % ==> termination proof established
som4_1(f, f, b, b).
    % ==> no proof found
som4_1(b, f, f, f).
    % ==> no proof found
som4_1(f, b, f, f).
    % ==> no proof found
som4_2(f, f, f, b).
    % ==> termination proof established
som4_2(f, b, b, f).
    % ==> termination proof established
som4_2(b, f, b, f).
    % ==> termination proof established
som4_2(b, b, f, f).
    % ==> no proof found
som4_2(f, f, b, f).
    % ==> no proof found

Tooltip: You can skip this comparison with termination analyzers by selecting "Comp. skipped" above

Analyzed program:

som3([],Bs,Bs).
som3(As,[],As).
som3([A|As],[B|Bs],[A+B|Cs]) :-
	som3(As,Bs,Cs).

som4_1(As,Bs,Cs,Ds) :-
	som3(As,Bs,Es),
	som3(Es,Cs,Ds).
som4_2(As,Bs,Cs,Ds):-
	som3(Es,Cs,Ds),
	som3(As,Bs,Es).